\begin{tabbing} guarded\_permutation($T$;$P$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=rel\_star($T$ List;($\lambda$$L_{1}$,$L_{2}$. $\exists$$i$:\{0..($\parallel$$L_{1}$$\parallel-$1)$^{-}$\}.\+ \\[0ex]$P$($L_{1}$,$i$) \& $L_{2}$ $=$ swap($L_{1}$;$i$;$i$+1) $\in$ $T$ List)) \- \end{tabbing}